$\forall$$A$,$T$:Type, $B$:(Id$\rightarrow$Type), $s$:$A$, $v$:$T$, ${\it tgf}$:(${\it tg}$:Id $\times$ ($A$$\rightarrow$$T$$\rightarrow$($B$(${\it tg}$) List))).
\\[0ex]sends{-}msgs($s$; $v$; ${\it tgf}$) $\in$ ((${\it tg}$:Id $\times$ $B$(${\it tg}$)) List)